型理論 インデックス
型理論
依存型理論
(
Martin-Löf型理論
)
型システム
型理論、依存型理論を学習する
型理論の証明では
帰納法
を使用したものがよく出てくる
帰納法
帰納法の原理
整礎帰納法
構造的帰納法
余帰納法
余帰納法の原理
判断
項
型
型宇宙
ソート
Calculus of Constructions
Calculus of Inductive Constructions(CIC)
型理論と他の領域で対応するものある系の話
型と集合
Sets as Types
,
Types as Sets
型と論理
カリー＝ハワード対応
Propositions as Types
ハイパードクトリン
ホモトピー型理論から様相論理へのルートを考える
Modal Homotopy Type Theory
がホモトピー型理論と様相論理をあわせたもの
型と圏論
型とホモトピー論
型をホモトピー的に扱う
型理論と論理と圏論
カリー／ハワード／ランベック対応
ハイパードクトリン
ホモトピー型理論と論理・集合・圏論など？の関係
型をホモトピー的に扱う
Homotopy Type Theory(HoTT)
Cubical Type Theory
Observational Type Theory
Modal Homotopy Type Theory
○○ as ○○
Sets as Types
,
Types as Sets
Propositions as Types
パラドックス関連
可述的
非可述的
集合論
ラッセルのパラドックス
型理論
ジラールのパラドックス
Hurkensのパラドックス
文献
型理論の文献
関連
形式手法
#インデックスページ
#ハブページ